package com.googlecode.kipler.satisfiability.completion.rule.formula;

import java.util.Iterator;

import com.googlecode.kipler.container.dl.FormulaCategory;
import com.googlecode.kipler.container.dl.PBox;
import com.googlecode.kipler.container.dl.WcsData;
import com.googlecode.kipler.satisfiability.completion.rule.CompletionRule;
import com.googlecode.kipler.satisfiability.completion.rule.formula.uniformnotation.AlphaFormula;
import com.googlecode.kipler.satisfiability.reasoner.UnsatisfiableException;
import com.googlecode.kipler.syntax.formula.Formula;


/**
 * This rule finds all the conjunctions in the current world and adds both
 * operands of a conjunction to the current world.
 * 
 * @author İnanç Seylan
 * 
 */
public class AlphaFormulaRule extends CompletionRule {

	private boolean applied;

	private FormulaCategory category;

	private AlphaFormula alpha;

	private String ruleName;

	private PBox pBox;

	public AlphaFormulaRule(FormulaCategory category, AlphaFormula alpha,
			String ruleName) {
		this.category = category;
		this.alpha = alpha;
		this.ruleName = ruleName;
	}

	/**
	 * For all formulae in this world, call
	 * {@link #decomposeConjunction(Formula)}.
	 * 
	 * @see tr.edu.ege.seagent.alcbi.satisfiability.frame.CompletionRule#apply()
	 */
	public void apply() throws UnsatisfiableException {
		applied = false;
		pBox = getWorld().getPBox();
		for (Iterator<Formula> i = pBox.formulaIterator(category); i.hasNext();) {
			Formula f = i.next();
			decomposeAlphaFormula(f);
		}
	}

	/**
	 * Any one operand or both operands of a conjunction can also be a
	 * conjunction. This method allows to handle multiple levels of conjunctive
	 * formulae by recursively calling itself on the operands of the
	 * (conjunctive) formula given.
	 * 
	 * @param f
	 *            The formula to be decomposed if it's a conjunction of course
	 */
	private void decomposeAlphaFormula(Formula f) throws UnsatisfiableException {
		alpha.setAlpha(f);
		if (alpha.isValid()) {
			Formula lhs = alpha.getAlpha1();
			Formula rhs = alpha.getAlpha2();
			WcsData wcsData = getWcs().getData();
			if (!getWorld().contains(lhs)) {
				applied = true;
				wcsData.getLogger().info(
						"WCS " + getWcs().getId() + " " + ruleName
								+ ": Adding " + lhs);
				wcsData.getDependencyManager().move(lhs, f);
				getWorld().add(lhs);
				decomposeAlphaFormula(lhs);
			}
			if (!getWorld().contains(rhs)) {
				applied = true;
				wcsData.getLogger().info(
						"WCS " + getWcs().getId() + " " + ruleName
								+ ": Adding " + rhs);
				wcsData.getDependencyManager().move(rhs, f);
				getWorld().add(rhs);
				decomposeAlphaFormula(rhs);
			}
		}
	}

	@Override
	public boolean isApplied() {
		return applied;
	}

}
